module Main where 

import System.IO
import Parser
import Lexer
import ModelChecker
import DirectApproach

yesno :: String -> IO Bool
yesno prompt = 
  do
    putStr (prompt ++ " y/n: ")
    hFlush stdout
    str <- getLine
    case str of
      "y" -> return True
      "n" -> return False
      _   -> do 
        putStrLn "Invalid input."              
        yesno prompt

getPOCTLFormula :: (Eq a, Show a) => HMM a -> IO ()
getPOCTLFormula hmm = 
  do
    putStrLn "\nEnter the POCTL* formula we are interested in."
    poctlF <- getLine
    let formulaTokens = lexerPOCTL poctlF 
    
    let poctlFormula = parsePOCTL formulaTokens
    
    putStr "\n"
    print poctlFormula
    putStr "\n"
    
    putStrLn "The states that satisfy it are:"
    print (satPOCTL hmm poctlFormula)
    continue <- yesno "\nDo you want to continue checking more specifications?"
    if continue 
      then getPOCTLFormula hmm 
      else return ()

main :: IO ()
main = 
  do      
    hSetBuffering stdout NoBuffering
    putStrLn "Enter the file name where the HMM is located."
    
    fname    <- getLine                -- Reads the file name
    contents <- readFile fname         -- Reads the contents of the file
    
    let tokens = lexer contents             
    
    let hmm = parse tokens
    
    getPOCTLFormula hmm